A:Type, B, C:(AType), eq:EqDecider(A), f:a:A fp B(a), g:a:A fp C(a), x:A, P:(a:AB(a)Prop),
Q:(a:AC(a)Prop).
(x:A. x  dom(g)  x  dom(f)  C(x)  B(x) & (P(x,g(x))  Q(x,g(x))))
 {g  f  (z != f(x)  P(y,z))  (z != g(x)  Q(y,z))} 

latex

Definitions	f  g, z != f(x)  P(a;z), {T}, x  dom(f), f(x), Top, Prop, a:A fp B(a), x. t(x), x(s), EqDecider(T), t  T, b, x(s1,s2), x:A. B(x), A & B, P  Q
Lemmas	deq wf, fpf wf, fpf-trivial-subtype-top, fpf-ap wf, fpf-dom wf, assert wf